[git] • Branch: master @ 50e93b6 • Head tags: v0.5-1-g50e93b6 • Compile time: 2018-08-29 12:18
in p + zero == p)
, QC.testProperty "addition with inverse" $
\x -> (let p = pfromList (x :: [(Int, [(Integer, Integer)])])
in p - p == zero)
]
qcModProps = testGroup "Module axioms"
[ QC.testProperty "first distributive law" $
\a x y -> (let p = pfromList (x :: [(Int, [(Integer, Integer)])])
q = pfromList (y :: [(Int, [(Integer, Integer)])])
in (a :: Int) *> (p + q) == a *> q + a *> p)
, QC.testProperty "second distributive law" $
\a b x -> (let p = pfromList (x :: [(Int, [(Integer, Integer)])])
in (a + b :: Int) *> p == a *> p + b *> p)
, QC.testProperty "multiplications commute" $
\a b x -> (let p = pfromList (x :: [(Int, [(Integer, Integer)])])
in (a * b :: Int) *> p == a *> (b *> p))
, QC.testProperty "multiplication by one" $
\x -> (let p = pfromList (x :: [(Int, [(Integer, Integer)])])
in (one :: Int) *> p == p)
]
qcRingProps = testGroup "Ring axioms"
[ QC.testProperty "multiplication is associative" $
\x y z -> (let p1 = pfromList (x :: [(Int, [(Integer, Integer)])])
p2 = pfromList (y :: [(Int, [(Integer, Integer)])])
p3 = pfromList (z :: [(Int, [(Integer, Integer)])])
in (p1 * p2) * p3 == p1 * (p2 * p3))
, QC.testProperty "left multiplication by one" $
\x -> (let p = pfromList (x :: [(Int, [(Integer, Integer)])])
in one * p == p)
, QC.testProperty "right multiplication by one" $
\x -> (let p = pfromList (x :: [(Int, [(Integer, Integer)])])
in p * one == p)
, QC.testProperty "distributive law" $
\x y z -> (let p1 = pfromList (x :: [(Int, [(Integer, Integer)])])
p2 = pfromList (y :: [(Int, [(Integer, Integer)])])
p3 = pfromList (z :: [(Int, [(Integer, Integer)])])
in p1 * (p2 + p3) == p1 * p2 + p1 * p3)
]
qcAlgebraProps = testGroup "Algebra axioms"
[ QC.testProperty "multiplications commute" $
\x y a -> (let p1 = pfromList (x :: [(Int, [(Integer, Integer)])])
p2 = pfromList (y :: [(Int, [(Integer, Integer)])])
in (a :: Int) *> (p1 * p2) == (a *> p1) * p2)